g:IMonoid, a, b, c:.
(a  b)
 (b < c)
 (E:({a..c}|g|).
 ( a  j < c. E(j)) = (( a  j < b. E(j)) * (E(b) * ( b+1  j < c. E(j))))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	, t  T, P  Q, x:A. B(x), P & Q, i  j < k, x. t(x), False, A, P  Q, P  Q, x f y, x(s), {i..j}, A  B, IMonoid
Lemmas	imon wf, le wf, grp car wf, int seg wf, mon itop unroll lo, mon itop wf, grp op wf, mon itop split